c:. ((c = 0  ))  ((1/c = 0  )) 

latex

Definitions	, t  T, A, P  Q, x:A. B(x), P & Q, P  Q, P  Q, b, (i = j), qeq(r;s), ff, i <z j, tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, if b then t else f fi , b, a <p b, a < b, r * s, False, (r/s), r < s, P  Q, S  T
Lemmas	rationals wf, not wf, qinv-positive, assert-qeq, qeq wf2, assert wf, not functionality wrt iff, qinv wf, int inc rationals, qmul wf, qless wf, qinv-negative, qless trichot qorder